/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=NGR25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]



␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY

␈↓ ↓H␈↓CS206  ␈↓ βZCOMPUTING WITH SYMBOLIC EXPRESSIONS  ␈↓ 
QFall 1977

␈↓ ↓H␈↓α␈↓ ¬
Solutions for Problem Set 2.


␈↓ ↓H␈↓αGeneral comments.

␈↓ ↓H␈↓        The␈αhomework␈αindicates␈αthat␈αpeople␈α
seem␈αto␈αbe␈αable␈αto␈α
use␈αthe␈αtwo␈αinductions␈αschemas␈α
and
␈↓ ↓H␈↓work␈αout␈α
the␈αmain␈α
steps␈αof␈α
a␈αproof.␈α
 The␈αmain␈α
difficulty␈αseems␈α
to␈αbe␈α
in␈αunderstanding␈α
how␈αto␈α
use
␈↓ ↓H␈↓the␈αfact␈α
that␈αsome␈α
of␈αthe␈α
variables␈αhave␈αrestricted␈α
ranges␈α(are␈α
sorted).␈α Since␈α
the␈αaxioms␈αare␈α
stated
␈↓ ↓H␈↓in␈αterms␈αof␈αsorted␈αvariables␈αit␈αis␈αimportant␈αto␈αunderstand␈αthe␈αimplications␈αof␈αthis␈αin␈αorder␈αnot␈αto
␈↓ ↓H␈↓prove␈αthings␈αwhich␈αare␈αin␈α
fact␈αfalse.␈α Therefore␈αin␈αpresenting␈αthe␈α
solutions␈αto␈αproblems␈α1␈αand␈α2,␈α
I
␈↓ ↓H␈↓will␈α
try␈α
to␈α
be␈αespecially␈α
carefull␈α
to␈α
point␈αout␈α
where␈α
it␈α
is␈αthat␈α
terms␈α
have␈α
to␈αbe␈α
shown␈α
to␈α
be␈α
of␈αa
␈↓ ↓H␈↓given␈αsort␈αin␈αorder␈αfor␈αthe␈αaxioms,␈αdefinitions,␈αand␈αtheorems␈αcan␈αbe␈αapplied.␈α The␈αproofs␈αwill␈αbe
␈↓ ↓H␈↓fairly␈α∂brief␈α∂in␈α∂other␈α∂respects␈α∂and␈α∂in␈α⊂particular␈α∂the␈α∂basic␈α∂LISP␈α∂axioms␈α∂will␈α∂often␈α⊂used␈α∂without
␈↓ ↓H␈↓comment.␈α Hopefully␈αthis␈αtogether␈αwith␈αthe␈αrevised␈αsection␈αof␈αChapter␈α3␈αwill␈αhelp␈αmake␈αthis␈αstyle
␈↓ ↓H␈↓of proof clearer.

␈↓ ↓H␈↓        Problem␈α3␈αis␈αworked␈αout␈αin␈αsome␈α
detail␈αas␈αmany␈αpeople␈αdid␈αnot␈αmake␈αa␈α
formal␈αconnection
␈↓ ↓H␈↓between the imitation and real predicates  and other details were frequently missed.

␈↓ ↓H␈↓        In␈αgrading␈αthe␈αhomework,␈αI␈αlooked␈αfor␈αcorrectness␈αof␈αthe␈αsteps␈αof␈αeach␈αproof␈αand␈αindicated
␈↓ ↓H␈↓places␈α∩where␈α⊃although␈α∩the␈α∩proof␈α⊃step␈α∩was␈α⊃correct␈α∩some␈α∩of␈α⊃the␈α∩necessary␈α⊃facts␈α∩had␈α∩not␈α⊃been
␈↓ ↓H␈↓established.␈α∂ No␈α∂number␈α⊂grade␈α∂was␈α∂given.␈α∂ If␈α⊂there␈α∂are␈α∂points␈α∂which␈α⊂you␈α∂still␈α∂are␈α∂not␈α⊂sure␈α∂of
␈↓ ↓H␈↓please ask.


␈↓ ↓H␈↓αProblem 1.

␈↓ ↓H␈↓        We will use the following facts about the operator < >:

␈↓ ↓H␈↓1.0             ␈↓↓∀x: islist <x>␈↓   and    ␈↓↓∀x u: <x> * u = x . u␈↓

␈↓ ↓H␈↓We␈α∞will␈α∞use␈α∞the␈α∞fact␈α∞that␈α
␈↓↓issexp␈α∞␈↓αa|␈↓↓u␈↓␈α∞and␈α∞␈↓↓issexp␈α∞␈↓αd|␈↓↓u␈↓␈α∞in␈α
the␈α∞case␈α∞that␈α∞␈↓↓¬␈↓αn|␈↓↓u␈↓␈α∞often␈α∞without␈α
explicit
␈↓ ↓H␈↓mention.␈α These␈αfacts␈αare␈αa␈αsimple␈αconsequence␈αof␈αthe␈αdefinitions␈αof␈α*,␈α<>␈αand␈αthe␈αLISP␈αaxioms.
␈↓ ↓H␈↓We␈αwill␈αalso␈αuse␈α
the␈αresult␈αof␈αProblem␈α1.i␈α
which␈αwas␈αproved␈αin␈α
class.␈α We␈αwill␈αsometimes␈αjustify␈α
a
␈↓ ↓H␈↓step saying "by definition"  which means by whatever function definition is relevant.


␈↓ ↓H␈↓αProof of 1.ii         ␈↓↓∀u: islist reverse1 u␈↓α

␈↓ ↓H␈↓Method: list induction with   ␈↓↓␈↓πF␈↓↓[u] ≡ islist reverse1 u␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓islist reverse1 u ≡ islist ␈↓¬NIL␈↓↓␈↓    ...by definition of ␈↓↓reverse1␈↓
␈↓ ↓H␈↓                        ≡ T   ...by the LISP axioms.
␈↓ ↓H␈↓␈↓ εH␈↓ 92


␈↓ ↓H␈↓Case  ␈↓↓¬␈↓αn|␈↓↓u␈↓ and ␈↓↓islist reverse1 ␈↓αd|␈↓↓u␈↓

␈↓ ↓H␈↓    ␈↓↓islist reverse1 u ≡ islist [reverse1 ␈↓αd|␈↓↓u * <␈↓αa|␈↓↓u>]␈↓   ...by definition  of ␈↓↓reverse1␈↓
␈↓ ↓H␈↓                        ≡  T   ...by induction hypothesis, ␈↓¬ISLIST-APPEND ␈↓and 1.0.


␈↓ ↓H␈↓αProof of 1.iii  ␈↓↓∀u: reverse u = reverse1 u␈↓α

␈↓ ↓H␈↓        We prove a slightly more general result, namely

␈↓ ↓H␈↓1.1             ␈↓↓∀u v: reverse1 u * v = rev[u,v]␈↓

␈↓ ↓H␈↓then taking ␈↓↓v␈↓ = ␈↓¬NIL␈↓ the desired result follows by 1.i  and the definition of ␈↓↓reverse.␈↓

␈↓ ↓H␈↓Method: list induction with   ␈↓↓␈↓πF␈↓↓[u] ≡ ∀v: reverse1 u * v = rev[u,v]␈↓.

␈↓ ↓H␈↓Case  ␈↓↓␈↓αn|␈↓↓u␈↓

␈↓ ↓H␈↓    ␈↓↓reverse1 ␈↓¬NIL␈↓↓ * v = v␈↓   ...by definition of ␈↓↓reverse1␈↓ and ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓                      ␈↓↓= rev[u,v]␈↓   ...by definition of ␈↓↓rev␈↓ .

␈↓ ↓H␈↓Case  ␈↓↓¬␈↓αn|␈↓↓u␈↓ and ␈↓↓∀v: reverse1 ␈↓αd|␈↓↓u * v = rev[␈↓αd|␈↓↓u,v]␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse1 u = reverse1 ␈↓αd|␈↓↓u * <␈↓αa|␈↓↓u>␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= rev[␈↓αd|␈↓↓u,<␈↓αa|␈↓↓u>]␈↓   ...by induction hypothesis and ␈↓↓islist <␈↓αa|␈↓↓u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= rev[u,␈↓¬NIL␈↓↓]␈↓   ...by definition.

␈↓ ↓H␈↓From here on we shall use ␈↓↓reverse␈↓ and ␈↓↓reverse1␈↓ interchangably.


␈↓ ↓H␈↓αProof of 1.v  ␈↓↓∀u v: [reverse[u * v] = reverse v * reverse u]␈↓α

␈↓ ↓H␈↓Method: list induction with ␈↓↓␈↓πF␈↓↓[u] ≡ ∀v: reverse[u * v] = reverse v * reverse u]␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse[␈↓¬NIL␈↓↓ * v] = reverse v␈↓   ...by ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓                   ␈↓↓= reverse v * ␈↓¬NIL␈↓↓␈↓   ...by 1.i
␈↓ ↓H␈↓                   ␈↓↓= reverse v * reverse ␈↓¬NIL␈↓↓␈↓   ...by definition.

␈↓ ↓H␈↓Case    ␈↓↓¬␈↓αn|␈↓↓u␈↓ and ␈↓↓∀v: reverse[␈↓αd|␈↓↓u * v] = reverse v * reverse ␈↓αd|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse[u * v] = reverse[␈↓αd|␈↓↓u * v] * <␈↓αa|␈↓↓u>␈↓   ...by definition, ␈↓¬CAR/CDR-APPEND ␈↓and ␈↓↓islist u*v␈↓
␈↓ ↓H␈↓                    ␈↓↓= [reverse v * reverse ␈↓αd|␈↓↓u] * <␈↓αa|␈↓↓u>␈↓   ...by induction hypothesis
␈↓ ↓H␈↓                    ␈↓↓= reverse v * [reverse ␈↓αd|␈↓↓u * <␈↓αa|␈↓↓u>]␈↓   ...by ␈↓¬ASSOC-APPEND ␈↓
␈↓ ↓H␈↓                ...here we need ␈↓↓islist reverse v␈↓, ␈↓↓islist reverse ␈↓αd|␈↓↓u␈↓ and ␈↓↓islist <␈↓αa|␈↓↓u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= reverse v * reverse u␈↓   ...by definition
␈↓ ↓H␈↓␈↓ εH␈↓ 93


␈↓ ↓H␈↓αProof of 1.iv   ␈↓↓∀u: reverse reverse u = u␈↓α

␈↓ ↓H␈↓Method: list induction with    ␈↓↓␈↓πF␈↓↓[u] ≡ reverse reverse u = u␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse reverse ␈↓¬NIL␈↓↓ = reverse ␈↓¬NIL␈↓↓ = ␈↓¬NIL␈↓↓␈↓   ... by definition

␈↓ ↓H␈↓Case    ␈↓↓¬␈↓αn|␈↓↓u␈↓ and ␈↓↓reverse reverse ␈↓αd|␈↓↓u = ␈↓αd|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓reverse reverse u = reverse[reverse ␈↓αd|␈↓↓u * <␈↓αa|␈↓↓u>]␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= reverse <␈↓αa|␈↓↓u> * reverse reverse ␈↓αd|␈↓↓u␈↓   ... by 1.v
␈↓ ↓H␈↓             ...here we need ␈↓↓islist reverse ␈↓αd|␈↓↓u␈↓ and ␈↓↓islist <␈↓αa|␈↓↓u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= <␈↓αa|␈↓↓u> * ␈↓αd|␈↓↓u␈↓   ...by induction hypothesis and computation  using ␈↓↓islist <␈↓αa|␈↓↓u>␈↓
␈↓ ↓H␈↓                    ␈↓↓= u␈↓   ...by 1.0 and the LISP axioms


␈↓ ↓H␈↓αProof of the ␈↓↓fringe␈↓α problem  ␈↓ ¬	␈↓↓∀x u: flat[x,u] = fringe x * u␈↓α

␈↓ ↓H␈↓Method: S-expression induction with   ␈↓↓␈↓πF␈↓↓[x] ≡ ∀u: flat[x,u] = fringe x * u␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αat|␈↓↓x␈↓:

␈↓ ↓H␈↓    ␈↓↓flat[x,u] = x . u␈↓    ...by definition
␈↓ ↓H␈↓              ␈↓↓= <x> * u␈↓   ... by 1.0
␈↓ ↓H␈↓              ␈↓↓= fringe x * u␈↓  ... by definition

␈↓ ↓H␈↓Case   ␈↓↓¬␈↓αat|␈↓↓x␈↓ and ␈↓↓∀u: flat[␈↓αd|␈↓↓x,u] = fringe ␈↓αd|␈↓↓x * u␈↓ :

␈↓ ↓H␈↓    ␈↓↓flat[x,u] = flat[␈↓αa|␈↓↓x,flat[␈↓αd|␈↓↓x,u]]␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= flat[␈↓αa|␈↓↓x,fringe ␈↓αd|␈↓↓x * u]␈↓   ...by induction hypothesis
␈↓ ↓H␈↓                    ␈↓↓= fringe ␈↓αa|␈↓↓x * [fringe ␈↓αd|␈↓↓x * u]␈↓   ...again by induction hypothesis
␈↓ ↓H␈↓                                            ...here we need ␈↓↓islist fringe ␈↓αd|␈↓↓x * u␈↓
␈↓ ↓H␈↓                    ␈↓↓= fringe x * u␈↓   ...by ␈↓¬ISTOT-APPEND ␈↓and definition of ␈↓↓fringe␈↓
␈↓ ↓H␈↓                           ...here we need ␈↓↓islist fringe ␈↓αd|␈↓↓x ␈↓ and ␈↓↓islist fringe ␈↓αa|␈↓↓x␈↓

␈↓ ↓H␈↓This ends Problem 1.


␈↓ ↓H␈↓αProblem 2.

␈↓ ↓H␈↓        In␈α
proving␈α
the␈α
desired␈α
fact␈α
about␈α
␈↓↓subst,␈↓␈α
␈↓↓sublis,␈↓␈α
and␈α
@␈α
we␈α
will␈α
use␈α
a␈α
new␈α
sort␈α∞␈↓↓slist.␈↓␈α
 The
␈↓ ↓H␈↓variables␈α∀␈↓↓s,␈↓␈α∀␈↓↓s1,␈↓␈α∪␈↓↓s2,␈↓␈α∀␈↓↓s3␈↓␈α∀range␈α∀over␈α∪the␈α∀domain␈α∀characterized␈α∪by␈α∀the␈α∀predicate␈α∀␈↓↓slist.␈↓␈α∪ We
␈↓ ↓H␈↓axiomatize slists as follows:

␈↓ ↓H␈↓2.1     ␈↓↓∀X: [slist X ≡ islist X ∧ [␈↓αn|␈↓↓X ∨ [¬␈↓αat|␈↓↓␈↓αa|␈↓↓X ∧ slist ␈↓αd|␈↓↓X]]]␈↓   ...X is a general variable.

␈↓ ↓H␈↓Thus ␈↓↓s␈↓ is either ␈↓¬NIL␈↓ or a list of nonatomic elements.   We shall also use the following facts.

␈↓ ↓H␈↓2.2     ␈↓↓∀x y: [occur[x,y] ≡ [x=y] ∨ [¬␈↓αat|␈↓↓y ∧ [occur[x, ␈↓αa|␈↓↓y] ∨ occur[x,␈↓αd|␈↓↓y]]]]␈↓
␈↓ ↓H␈↓2.3     ␈↓↓∀x s: [␈↓αn|␈↓↓assoc[x,s] ∨ [issexp assoc[x,s] ∧ ¬␈↓αat|␈↓↓assoc[x,s]]]␈↓
␈↓ ↓H␈↓␈↓ εH␈↓ 94


␈↓ ↓H␈↓2.4     ␈↓↓∀s1 s2:  slist s1 * s2␈↓
␈↓ ↓H␈↓2.5     ␈↓↓∀z s1 s2: [assoc[z,s1*s2] = ␈↓αif␈↓↓ ␈↓αn|␈↓↓assoc[z,s1] ␈↓αthen␈↓↓ assoc[z,s2] ␈↓αelse␈↓↓ assoc[z,s1]]␈↓
␈↓ ↓H␈↓2.6     ␈↓↓∀x y z: issexp subst[x, y, z]␈↓
␈↓ ↓H␈↓2.7     ␈↓↓∀x,s: issexp sublis[x,s]␈↓
␈↓ ↓H␈↓2.8     ␈↓↓∀s1 s2: slist subsub[s1,s2]␈↓
␈↓ ↓H␈↓        ␈↓↓∀s1 s2:  ¬␈↓αn|␈↓↓s1 ⊃ ¬␈↓αn|␈↓↓subsub[s1,s2]␈↓
␈↓ ↓H␈↓        ␈↓↓∀s1 s2:  ¬␈↓αn|␈↓↓s1 ⊃ ␈↓αd|␈↓↓subsub[s1,s2] = subsub[␈↓αd|␈↓↓s1,s2]␈↓
␈↓ ↓H␈↓2.9     ␈↓↓∀s1 s2: slist s1@s2␈↓

␈↓ ↓H␈↓The␈α
proof␈α
of␈α
2.2␈α
is␈α
outlined␈α
in␈α
the␈α
notes␈α
and␈α
2.3␈α
-␈α
2.9␈α
can␈α
be␈α
proved␈α
by␈α
straight␈α
forward␈α
list␈αor␈α
S-
␈↓ ↓H␈↓expression induction using the LISP axioms function definitions and 2.1.


␈↓ ↓H␈↓αProof of 2.i   ␈↓↓∀x y z: subst[x, y, z] = sublis[z, <x,y>]␈↓α

␈↓ ↓H␈↓Method: S-expression induction with   ␈↓↓␈↓πF␈↓↓[z] ≡ ∀x y: subst[x,y,z] = sublis[z,<x.y>]␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αat|␈↓↓z␈↓:

␈↓ ↓H␈↓    ␈↓↓subst[x,y,z] = ␈↓αif␈↓↓ y=z ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ z␈↓    ...by definition of ␈↓↓subst␈↓
␈↓ ↓H␈↓    ␈↓↓sublis[z,<y.x>] = {assoc[z,<y.x>]}[λz1: ␈↓αif␈↓↓ ␈↓αn|␈↓↓z1 ␈↓αthen␈↓↓ z ␈↓αelse␈↓↓ ␈↓αd|␈↓↓z1]␈↓   ... by definition of ␈↓↓sublis␈↓
␈↓ ↓H␈↓                    ␈↓↓= ␈↓αif␈↓↓ y≠z ␈↓αthen␈↓↓ z ␈↓αelse␈↓↓ ␈↓αd|␈↓↓y.x␈↓    ...by computation since ␈↓↓slist <y.x>␈↓.

␈↓ ↓H␈↓Case ␈↓↓¬␈↓αat|␈↓↓z␈↓ and ␈↓↓∀x y: [subst[x, y, ␈↓αa|␈↓↓z] = sublis[␈↓αa|␈↓↓z, <y.x>] ∧ subst[x,y,␈↓αd|␈↓↓z] = sublis[␈↓αd|␈↓↓z,<y.x>]]␈↓

␈↓ ↓H␈↓    ␈↓↓subst[x,y,z] = subst[x,y,␈↓αa|␈↓↓z] . subst[x,y,␈↓αd|␈↓↓z]␈↓    ...by definition of ␈↓↓subst␈↓
␈↓ ↓H␈↓                    ␈↓↓= sublis[␈↓αa|␈↓↓z, <y.x>] . sublis[␈↓αd|␈↓↓z,<y.x>]␈↓    ...by induction hypothesis
␈↓ ↓H␈↓                    ␈↓↓= sublis[z,<y.x>]␈↓    ...by definition of ␈↓↓sublis.␈↓


␈↓ ↓H␈↓        Before proving (ii) we prove some lemmas.  Namely

␈↓ ↓H␈↓2.10    ␈↓↓∀z s1 s2: [␈↓αn|␈↓↓assoc[z, s1] ⊃ assoc[z, s1@s2] = assoc[z,s2]]␈↓
␈↓ ↓H␈↓2.11    ␈↓↓∀z s1 s2:  [¬␈↓αn|␈↓↓assoc[z,s1] ⊃ ¬␈↓αn|␈↓↓assoc[z,s1@s2] ∧ ␈↓αd|␈↓↓assoc[z,s1@s2] = sublis[␈↓αd|␈↓↓assoc[z,s1],s2]␈↓

␈↓ ↓H␈↓These␈αare␈αfairly␈αsimple␈αconsequences␈αof␈αthe␈αfacts␈αmentioned␈αat␈αthe␈αbeginning␈αof␈αthis␈αproblem␈α
and
␈↓ ↓H␈↓the following statement:

␈↓ ↓H␈↓2.12    ␈↓↓∀z s1 s2: [␈↓αn|␈↓↓assoc[z, s1] ≡ ␈↓αn|␈↓↓assoc[z,subsub[s1,s2]]]␈↓
␈↓ ↓H␈↓                ␈↓↓∧ [¬␈↓αn|␈↓↓assoc[z,s1] ⊃ ␈↓αd|␈↓↓assoc[z,subsub[s1,s2] = sublis[␈↓αd|␈↓↓assoc[z,s1],s2]]␈↓


␈↓ ↓H␈↓αProof of 2.12.

␈↓ ↓H␈↓Method:  list induction on ␈↓↓s1.␈↓

␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓s1␈↓:

␈↓ ↓H␈↓    Both sides of the equivalence reduce to ␈↓↓␈↓αn|␈↓↓␈↓¬NIL␈↓↓␈↓ and the left hand side of ⊃ is F.
␈↓ ↓H␈↓␈↓ εH␈↓ 95


␈↓ ↓H␈↓Case ␈↓↓¬␈↓αn|␈↓↓s1␈↓ and ␈↓↓∀z s2: [␈↓αn|␈↓↓assoc[z, ␈↓αd|␈↓↓s1] ≡ ␈↓αn|␈↓↓assoc[z,subsub[␈↓αd|␈↓↓s1,s2]]]␈↓
␈↓ ↓H␈↓                   ␈↓↓∀z s2: [¬␈↓αn|␈↓↓assoc[z,␈↓αd|␈↓↓s1] ⊃ ␈↓αd|␈↓↓assoc[z,subsub[␈↓αd|␈↓↓s1,s2] = sublis[␈↓αd|␈↓↓assoc[z,␈↓αd|␈↓↓s1], s2]]␈↓

␈↓ ↓H␈↓    ␈↓↓assoc[z,subsub[s1,s2]] = ␈↓αif␈↓↓ z=␈↓αaa|␈↓↓subsub[s1,s2] ␈↓αthen␈↓↓ ␈↓αa|␈↓↓subsub[s1,s2] ␈↓αelse␈↓↓ assoc[z,subsub[␈↓αd|␈↓↓s1,s2]]␈↓
␈↓ ↓H␈↓           ...by definition of ␈↓↓assoc␈↓
␈↓ ↓H␈↓           ...here we need ␈↓↓slist subsub[s1,s2]␈↓, ␈↓↓¬␈↓αn|␈↓↓subsub[s1,s2]␈↓ and ␈↓↓␈↓αd|␈↓↓subsub[s1,s2] = subsub[␈↓αd|␈↓↓s1,s2]␈↓
␈↓ ↓H␈↓                ␈↓↓= ␈↓αif␈↓↓ z = ␈↓αaa|␈↓↓s1 ␈↓αthen␈↓↓ [␈↓αaa|␈↓↓s1 . sublis[␈↓αda|␈↓↓s1,s2]] ␈↓αelse␈↓↓ assoc[z, subsub[␈↓αd|␈↓↓s1,s2]]␈↓
␈↓ ↓H␈↓           ...here we need in addition, 2.1, the definition of ␈↓↓subsub␈↓ and ␈↓↓issexp sublis[␈↓αda|␈↓↓s1,s2]␈↓

␈↓ ↓H␈↓Subcase  ␈↓↓z = ␈↓αaa|␈↓↓s1 ␈↓:  the result follows from the definitions by computation.

␈↓ ↓H␈↓Subcase   ␈↓↓z ≠ ␈↓αaa|␈↓↓s1␈↓: the result follows from the induction hypothesis and definition of ␈↓↓assoc.␈↓


␈↓ ↓H␈↓αProof of 2.10

␈↓ ↓H␈↓Assume: ␈↓↓␈↓αn|␈↓↓assoc[z,s1]␈↓

␈↓ ↓H␈↓    ␈↓↓␈↓αn|␈↓↓assoc[z, subsub[s1,s2]]␈↓    ... by 2.12
␈↓ ↓H␈↓    ␈↓↓assoc[z,subsub[s1,s2]*s2] = assoc[z,s1@s2] = assoc[z,s2]␈↓   ...by 2.5 and definition of @.


␈↓ ↓H␈↓αProof of 2.11

␈↓ ↓H␈↓Assume: ␈↓↓¬␈↓αn|␈↓↓assoc[z,s1]␈↓

␈↓ ↓H␈↓    ␈↓↓¬␈↓αn|␈↓↓assoc[z,subsub[s1,s2]]␈↓    ...by 2.12
␈↓ ↓H␈↓    ␈↓↓assoc[z,s1@s2] = assoc[z,subsub[s1,s2]]␈↓    ...by 2.5 and definition of @

␈↓ ↓H␈↓The result then follows from the second part of 2.12 and ␈↓¬NOTNIL-APPEND. ␈↓


␈↓ ↓H␈↓αProof of 2.ii   ␈↓↓∀z s1 s2: sublis[z,s1@s2] = sublis[sublis[z,s1],s2]␈↓α.

␈↓ ↓H␈↓Method: S-expression induction with ␈↓↓␈↓πF␈↓↓[z] ≡ ∀s1 s2: sublis[z,s1@s2] = sublis[sublis[z,s1],s2]␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αat|␈↓↓z␈↓:

␈↓ ↓H␈↓    ␈↓↓sublis[z,s1@s2] = {assoc[z,s1@s2]}[λz1: ␈↓αif␈↓↓ ␈↓αn|␈↓↓z1 ␈↓αthen␈↓↓ z ␈↓αelse␈↓↓ ␈↓αd|␈↓↓z1]␈↓
␈↓ ↓H␈↓    ␈↓↓sublis[z,s1] = {assoc[z,s1]}[λz1: ␈↓αif␈↓↓ ␈↓αn|␈↓↓z1 ␈↓αthen␈↓↓ z ␈↓αelse␈↓↓ ␈↓αd|␈↓↓z1]␈↓

␈↓ ↓H␈↓If ␈↓↓␈↓αn|␈↓↓assoc[z,s1]␈↓ the result follows from 2.10 and if ␈↓↓¬␈↓αn|␈↓↓assoc[z,s1]␈↓ the result follows from 2.11.

␈↓ ↓H␈↓Case  ␈↓↓¬␈↓αat|␈↓↓z␈↓ and ␈↓↓∀s2: [sublis[␈↓αa|␈↓↓z, s1@s2] = sublis[sublis[␈↓αa|␈↓↓z,s1],s2]␈↓
␈↓ ↓H␈↓                ∧ ␈↓↓∀s2: [sublis[␈↓αd|␈↓↓z, s1@s2] = sublis[sublis[␈↓αd|␈↓↓z,s1],s2]␈↓

␈↓ ↓H␈↓    ␈↓↓sublis[z,s1@s2] = sublis[␈↓αa|␈↓↓z,s1@s2] . sublis[␈↓αd|␈↓↓z,s1@s2]␈↓   ...by definition
␈↓ ↓H␈↓                    ␈↓↓= sublis[sublis[␈↓αa|␈↓↓z,s1],s2] . sublis[sublis[␈↓αd|␈↓↓z,si],s2]␈↓    ...by induction
␈↓ ↓H␈↓                    ␈↓↓= sublis[sublis[z,s1],s2]␈↓   ... by definition of ␈↓↓sublis␈↓
␈↓ ↓H␈↓           ...here we need ␈↓↓issexp sublis[␈↓αa|␈↓↓z,s1]␈↓ and ␈↓↓issexp sublis[␈↓αd|␈↓↓z,s1]␈↓
␈↓ ↓H␈↓␈↓ εH␈↓ 96


␈↓ ↓H␈↓αProof of 2.iii ␈↓↓∀z s1 s2 s3: sublis[z, s1@[s2@s3]] = sublis[z, [s1@s2]@s3]]␈↓α

␈↓ ↓H␈↓        This is a direct consequence of 2.ii and ␈↓↓slist s1@s2␈↓ as follows:

␈↓ ↓H␈↓                ␈↓↓sublis[z, s1@[s2@s3]] = sublis[sublis[z,s1],s2@s3] ␈↓
␈↓ ↓H␈↓                                ␈↓↓= sublis[sublis[sublis[z,s1],s2],s3]␈↓
␈↓ ↓H␈↓                                ␈↓↓= sublis[sublis[z,s1@s2],s3]␈↓
␈↓ ↓H␈↓                                ␈↓↓= sublis[z, [s1@s2]@s3]␈↓


␈↓ ↓H␈↓αProof of 2.iv  ␈↓↓∀x y z: [¬occur[y,z] ⊃ subst[x,y,z] = z]␈↓α

␈↓ ↓H␈↓Method: S-expression induction with  ␈↓↓␈↓πF␈↓↓[z] ≡ ∀x y: [¬occur[y,z] ⊃ subst[x,y,z] = z]␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αat|␈↓↓z␈↓:

␈↓ ↓H␈↓    ␈↓↓¬occur[y,z] ≡ y≠z␈↓ and ␈↓↓subst[x,y,z] = ␈↓αif␈↓↓ y = z ␈↓αthen␈↓↓ x ␈↓αelse␈↓↓ z␈↓ so ␈↓πF␈↓ holds.

␈↓ ↓H␈↓Case ␈↓↓¬␈↓αat|␈↓↓z␈↓ and ␈↓↓∀x y: [¬occur[y, ␈↓αa|␈↓↓z] ⊃ subst[x,y,␈↓αa|␈↓↓z] = ␈↓αa|␈↓↓z ∧  [¬occur[y, ␈↓αd|␈↓↓z] ⊃ subst [x,y,␈↓αd|␈↓↓z]]␈↓

␈↓ ↓H␈↓    ␈↓↓¬occur[y,z] ≡ y≠z ∧ ¬occur[y,␈↓αa|␈↓↓z] ∧ ¬occur[y,␈↓αd|␈↓↓z]␈↓
␈↓ ↓H␈↓    ␈↓↓subst[x,y,z] = subst[x,y,␈↓αa|␈↓↓z] . subst[x,y,␈↓αd|␈↓↓z]␈↓    ...by definition
␈↓ ↓H␈↓                 ␈↓↓= ␈↓αa|␈↓↓z . ␈↓αd|␈↓↓z␈↓   ...by induction hypothesis
␈↓ ↓H␈↓                 ␈↓↓= z␈↓

␈↓ ↓H␈↓␈↓αProof  of  2.v␈↓ ␈↓↓∀x  x1  y  y1  z:  [y ≠  y1  ∧  ¬occur[y,  x1]]  ⊃ ␈↓
␈↓ ↓H␈↓                                    ␈↓↓subst[x1,y1,subst[x,y,z]] = subst[subst[x1,y1,x],y,subst[x1,y1,z]]␈↓

␈↓ ↓H␈↓Method: S-expression induction on ␈↓↓z.␈↓

␈↓ ↓H␈↓Case ␈↓↓␈↓αat|␈↓↓z␈↓:

␈↓ ↓H␈↓    ␈↓↓subst[x1,y1,subst[x,y,z]] = ␈↓αif␈↓↓ y=z ␈↓αthen␈↓↓ subst[x1,y1,x] ␈↓αelse␈↓↓ ␈↓αif␈↓↓ y1=z ␈↓αthen␈↓↓ x1 ␈↓αelse␈↓↓ z␈↓

␈↓ ↓H␈↓    ␈↓↓subst[subst[x1,y1,x],y,subst[x1,y1,z]] ␈↓
␈↓ ↓H␈↓                ␈↓↓= ␈↓αif␈↓↓ y1=z ␈↓αthen␈↓↓ ␈↓αif␈↓↓ y=x1 ␈↓αthen␈↓↓ subst[x1,y1,x] ␈↓αelse␈↓↓ x1␈↓
␈↓ ↓H␈↓                            ␈↓↓␈↓αelse␈↓↓ ␈↓αif␈↓↓ y=z ␈↓αthen␈↓↓ subst[x1,y1,x] ␈↓αelse␈↓↓ z␈↓
␈↓ ↓H␈↓                ␈↓↓=␈↓αif␈↓↓ y1=z ␈↓αthen␈↓↓ x1 ␈↓αelse␈↓↓ ␈↓αif␈↓↓ y=z ␈↓αthen␈↓↓ subst[x1,y1,x] ␈↓αelse␈↓↓ z␈↓   ...since  ␈↓↓¬occur[y,x1]␈↓

␈↓ ↓H␈↓The result now follows by a simple case analysis since ␈↓↓y=z␈↓ and ␈↓↓y1=z␈↓ can not both be true.

␈↓ ↓H␈↓Case ␈↓↓¬␈↓αat|␈↓↓z␈↓ and ␈↓↓∀x  x1  y  y1:  [y  ≠  y1  ∧  ¬occur[y,  x1]]  ⊃␈↓
␈↓ ↓H␈↓        ␈↓↓subst[x1,y1,subst[x,y,␈↓αa|␈↓↓z] = subst[subst[x1,y1,x],y,subst[x1,y1,␈↓αa|␈↓↓z]]␈↓
␈↓ ↓H␈↓        ␈↓↓∧ subst[x1,y1,subst[x,y,␈↓αd|␈↓↓z] = subst[subst[x1,y1,x],y,subst[x1,y1,␈↓αd|␈↓↓z]]]␈↓

␈↓ ↓H␈↓    ␈↓↓subst[x1,y1,subst[x,y,z]] = subst[x1,y1,subst[x,y,␈↓αa|␈↓↓z] . subst[x,y,␈↓αd|␈↓↓z]]␈↓
␈↓ ↓H␈↓                ␈↓↓= subst[x1,y1,subst[x,y,␈↓αa|␈↓↓z]] . subst[x1,y1,[subst[x,y,␈↓αd|␈↓↓z]]␈↓
␈↓ ↓H␈↓                      ...here we need ␈↓↓issexp subst[x,y,␈↓αa|␈↓↓z]␈↓ and ␈↓↓issexp subst[x,y,␈↓αd|␈↓↓z]␈↓
␈↓ ↓H␈↓                ␈↓↓= subst[subst[x1,y1,x],y,subst[x1,y1,␈↓αa|␈↓↓z]] . subst[subst[x1,y1,x],y,subst[x1,y1,␈↓αd|␈↓↓z]]␈↓
␈↓ ↓H␈↓                ␈↓↓= subst[subst[x1,y1,x],y,subst[x1,y1,z]]␈↓
␈↓ ↓H␈↓␈↓ εH␈↓ 97


␈↓ ↓H␈↓This completes problem 2.


␈↓ ↓H␈↓αProblem 3.

␈↓ ↓H␈↓        We wish to prove the following two statements:

␈↓ ↓H␈↓(i)     ␈↓↓∀u v: andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]␈↓

␈↓ ↓H␈↓(ii)    ␈↓↓∀u: andlis[u,phi] ≡ andlis[reverse u,phi]␈↓

␈↓ ↓H␈↓where␈α∂␈↓↓phi␈↓␈α∂is␈α∂a␈α∂unary␈α∂predicate.␈α∂ (The␈α∂use␈α∂of␈α∂␈↓↓p␈↓␈α∂in␈α∂the␈α∂original␈α∂porblem␈α∂statement␈α∂was␈α⊂a␈α∂poor
␈↓ ↓H␈↓choice␈α
as␈α
␈↓↓p␈↓␈α
is␈α∞designated␈α
in␈α
Chapter␈α
3␈α
as␈α∞a␈α
variable␈α
of␈α
type␈α
␈↓↓istv.)␈↓␈α∞ Note␈α
that␈α
even␈α
to␈α∞state␈α
this
␈↓ ↓H␈↓problem␈α
requires␈αan␈α
extension␈αto␈α
the␈αsyntax␈α
of␈α
our␈αlanguage␈α
in␈αorder␈α
to␈αallow␈α
functions␈αthat␈α
have
␈↓ ↓H␈↓functions␈α
as␈α
arguments.␈α
 In␈α∞the␈α
problem␈α
␈↓↓phi␈↓␈α
is␈α∞considered␈α
as␈α
a␈α
parameter.␈α∞ (Quantification␈α
over
␈↓ ↓H␈↓predicates is not allowed.)

␈↓ ↓H␈↓        The␈α∞strategy␈α∞for␈α∂doing␈α∞the␈α∞proof␈α∂is␈α∞as␈α∞follows.␈α∂ We␈α∞define␈α∞an␈α∂imitation␈α∞of␈α∞␈↓↓andlis␈↓␈α∂by␈α∞the
␈↓ ↓H␈↓following axioms.

␈↓ ↓H␈↓3.1     ␈↓↓∀u: [aandlis[u,pphi] = nnull u oor [pphi ␈↓αa|␈↓↓u aand aandlis[␈↓αd|␈↓↓u,pphi]]␈↓
␈↓ ↓H␈↓3.2     ␈↓↓∀u: isetv aandlis ␈↓αd|␈↓↓u␈↓
␈↓ ↓H␈↓3.3     ␈↓↓∀u: isetv pphi ␈↓αa|␈↓↓u␈↓
␈↓ ↓H␈↓3.4     ␈↓↓∀x: istv pphi x␈↓
␈↓ ↓H␈↓3.5     ␈↓↓∀x: [phi x ≡ pphi x=␈↓¬TT␈↓↓]␈↓
␈↓ ↓H␈↓3.6     ␈↓↓∀u: [andlis[u,phi] ≡ aandlis[u,pphi] = ␈↓¬TT␈↓↓]␈↓

␈↓ ↓H␈↓Here␈α
␈↓↓nnull␈↓␈α
is␈α
defined␈α
similarly␈αto␈α
␈↓↓aatom␈↓␈α
and␈α
we␈α
assume␈αthe␈α
analagous␈α
results␈α
such␈α
as␈α␈↓¬TVNNUL,␈α
␈↓and
␈↓ ↓H␈↓␈↓¬EQNNUL.␈α␈↓␈α3.2␈αand␈α3.3␈αare␈αneeded␈αinorder␈αto␈α
be␈αable␈αto␈αuse␈αthe␈αdefinitions␈αof␈α␈↓↓aand␈↓␈αand␈α␈↓↓oor␈↓␈α
in␈αthe
␈↓ ↓H␈↓case ␈↓↓␈↓αn|␈↓↓u␈↓. Using these axioms we prove

␈↓ ↓H␈↓3.7     ␈↓↓∀u: istv aandlis[u,pphi]␈↓

␈↓ ↓H␈↓from which we get (using ␈↓¬EQAAND ␈↓␈↓¬EQOOR ␈↓etc., and the above axioms)  that

␈↓ ↓H␈↓3.8     ␈↓↓∀u: [andlis[u,phi] ≡ ␈↓αn|␈↓↓u ∨ [phi ␈↓αa|␈↓↓u ∧ andlis[␈↓αd|␈↓↓u,phi]]␈↓.

␈↓ ↓H␈↓This last statement is used together with list induction to prove the desired results.


␈↓ ↓H␈↓αProof of 3.7

␈↓ ↓H␈↓Method: list induction with ␈↓↓␈↓πF␈↓↓[u] ≡ istv aandlis[u,pphi]␈↓.
␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓aandlis[u,pphi] = ␈↓¬TT␈↓↓␈↓   ...by  definitions of ␈↓↓nnull,␈↓ ␈↓↓aand,␈↓ ␈↓↓oor,␈↓ 3.1, 3.2 and 3.3 .
␈↓ ↓H␈↓    ␈↓↓istv ␈↓¬TT␈↓↓␈↓

␈↓ ↓H␈↓Case ␈↓↓¬␈↓αn|␈↓↓u␈↓  and ␈↓↓istv aandlis[␈↓αd|␈↓↓u,pphi]␈↓:

␈↓ ↓H␈↓    ␈↓↓istv [pphi ␈↓αa|␈↓↓u aand aandlis[␈↓αd|␈↓↓u,pphi]␈↓   ...by induction, ␈↓¬TVAND ␈↓and 3.4
␈↓ ↓H␈↓␈↓ εH␈↓ 98


␈↓ ↓H␈↓    ␈↓↓istv [nnull u]␈↓   ..by remarks above
␈↓ ↓H␈↓    ␈↓↓istv aandlis[u,pphi]␈↓   ...by definition and ␈↓¬TVOOR. ␈↓


␈↓ ↓H␈↓αProof of 3.i.

␈↓ ↓H␈↓Method: list induction with  ␈↓↓␈↓πF␈↓↓[u] ≡ ∀v: [andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]]␈↓

␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓andlis[u*␈↓¬NIL␈↓↓,phi] ≡ andlis[u,phi]␈↓   ...by ␈↓¬NIL-APPEND ␈↓
␈↓ ↓H␈↓                         ␈↓↓≡ andlis[u,phi] ∧ andlis[␈↓¬NIL␈↓↓,phi]␈↓  ...by 3.8

␈↓ ↓H␈↓Case ␈↓↓¬␈↓αn|␈↓↓u␈↓ and ␈↓↓∀v: andlis[␈↓αd|␈↓↓u*v,phi] ≡ andlis[␈↓αd|␈↓↓u,phi] ∧ andlis[v,phi]␈↓

␈↓ ↓H␈↓    ␈↓↓andlis[u*v,phi] ≡ phi ␈↓αa|␈↓↓u ∧ andlis[␈↓αd|␈↓↓u*v,phi]␈↓    ...by ␈↓¬CAR/CDR-APPEND, ␈↓␈↓¬ISTOT-APPEND, ␈↓and 3.8.
␈↓ ↓H␈↓                ␈↓↓≡ phi ␈↓αa|␈↓↓u ∧ andlis[␈↓αd|␈↓↓u,phi] ∧ andlis[v,phi]␈↓    ...by the induction hypothesis
␈↓ ↓H␈↓                ␈↓↓≡ andlis[u,phi] ∧ andlis[v,phi]␈↓    ...by 3.8.



␈↓ ↓H␈↓αProof of 3.ii .

␈↓ ↓H␈↓Method: list induction with  ␈↓↓␈↓πF␈↓↓[u] ≡ [andlis[u,phi] ≡ andlis[reverse u,phi]]␈↓.

␈↓ ↓H␈↓Case ␈↓↓␈↓αn|␈↓↓u␈↓:

␈↓ ↓H␈↓    ␈↓↓andlis[reverse ␈↓¬NIL␈↓↓,phi] ≡ andlis[␈↓¬NIL␈↓↓,phi]␈↓   ...by definition of ␈↓↓reverse␈↓

␈↓ ↓H␈↓Case ␈↓↓¬␈↓αn|␈↓↓u␈↓ and ␈↓↓andlis[reverse ␈↓αd|␈↓↓u,phi] ≡ andlis[␈↓αd|␈↓↓u,phi]␈↓:

␈↓ ↓H␈↓    ␈↓↓andlis[reverse u,phi] ≡ andlis[reverse ␈↓αd|␈↓↓u * <␈↓αa|␈↓↓u>,phi]␈↓    ...by definition of ␈↓↓reverse␈↓
␈↓ ↓H␈↓                ␈↓↓≡ andlis[reverse ␈↓αd|␈↓↓u,phi] ∧ andlis[<␈↓αa|␈↓↓u>,phi]␈↓    ...by (i)
␈↓ ↓H␈↓                        ...here we need ␈↓↓islist reverse ␈↓αd|␈↓↓u␈↓ and ␈↓↓islist <␈↓αa|␈↓↓u>␈↓
␈↓ ↓H␈↓                ␈↓↓≡ andlis[<␈↓αa|␈↓↓u>,phi] ∧ andlis[␈↓αd|␈↓↓u,phi]␈↓    ...by induction hypothesis
␈↓ ↓H␈↓                ␈↓↓≡ andlis[u,phi]␈↓    ...by  3.8 and properties of <>.

␈↓ ↓H␈↓This completes Problem 3.